Reasoning about orchestrations of web services using partial correctness

摘要

A service is a remote computational facility which is made available for general use by means of a\udwide-area network. Several types of service arise in practice: stateless services, shared state services and services\udwith states which are customised for individual users. A service-based orchestration is a multi-threaded compu-\udtation which invokes remote services in order to deliver results back to a user (publication). In this paper a means\udof specifying services and reasoning about the correctness of orchestrations over\udstateless\udservices is presented.\udAs web services are potentially unreliable the termination of even finite orchestrations cannot be guaranteed.\udFor this reason a partial-correctness powerdomain approach is proposed to capture the semantics of recursive\udorchestrations.